Denotational Semantics of Dependent Type Theory 25

Info. This is a reading course in Denotational Semantics of (Dependent) Type Theory offered as an instance of Specialization in Logic.

Syllabus. (Dependent) Type theory. Categories with Families. Locally cartesian closed categories. Clans and generalized algebraic theories. Natural models. Comprehension categories. Representable map categories.

Audience and Prerequisites. A good knowledge of the language of category theory is a prerequisite for the audience.

• Category Theory in Context by Emily Riehl.

Bibliography.

• Introduction to Homotopy Type Theory by Egbert Rijke.

  Chap 1. Pages 1-99.

• Syntax and Semantics of Dependent Types by Martin Hofmann.

• Natural models of homotopy type theory by Steve Awodey.

• On the interpretation of Type Theory in locally cartesian closed categories by Martin Hofmann.

• Duality for Clans: an Extension of Gabriel-Ulmer Duality by Jonas Frey.

• A 2-categorical analysis of context comprehension by Greta Coraglia and Jacopo Emmenegger.

• A General Framework for the Semantics of Type Theory by Taichi Uemura.

Comments. The course is dense, and has no intention of completely cover the bibliography above. Instead, one of its main intents is to introduce the students to this corpus of knowledge, making sure that they reach a sufficient level of independence and maturity. When approaching the material above for the first time, we reccomend to skip the forth and last item in the Bibliography above.